Inference at * 
Iof proof for Lemma adjacent-before:


  T:Type, L:(T List), x, y:T. adjacent(T;L;x;y)  x before y  L 

latex

 by ((RepUR``adjacent l_before sublist`` 0) 
CollapseTHEN (((MaAuto) 
CollapseTHEN (((ExRepD) 

CoCollapseTHEN (Auto')))))) 

latex

C1: 

C1: 1. T : Type
C1: 2. L : T List
C1: 3. x : T
C1: 4. y : T
C1: 5. i : {0..(||L|| - 1)}
C1: 6. x = L[i]
C1: 7. y = L[(i+1)]
C1:   f:{0..2}{0..||L||}. (increasing(f;2) & (j:{0..2}. [x; y][j] = L[(f(j))]))
C.

Definitions	adjacent(T;L;x;y), x before y  l, L1  L2, P  Q, (x  l), [car / cdr], [], f(a), n - m, , l[i], n+m, #$n, t  T, {x:A| B(x)} , , type List, Type, P & Q, s = t, increasing(f;k), {i..j}, ||as||, i  j , x:A. B(x), x:AB(x), x:A. B(x), x:A  B(x)
Lemmas	increasing wf, int seg wf